Search for: All records

Many synthesis and verification problems can be reduced to determining the truth of formulas over the real numbers. These formulas often involve constraints with integrals in them. To this end, we extend the framework of δ-decision procedures with techniques for handling integrals of user-specified real functions. We implement this decision procedure in the tool ∫dReal, which is built on top of dReal. We evaluate ∫dReal on a suite of problems that include formulas verifying the fairness of algorithms and the privacy and the utility of privacy mechanisms and formulas that synthesize parameters for the desired utility of privacy mechanisms. The performance of the tool in these experiments demonstrates the effectiveness of ∫dReal. 

Security properties of real-time systems often involve reasoning about hyper-properties, as opposed to properties of single executions or trees of executions. These hyper-properties need to additionally be expressive enough to reason about real-time constraints. Examples of such properties include information flow, side channel attacks and service-level agreements. In this paper we study computational problems related to a branching-time, hyper-property extension of metric temporal logic (MTL) that we call HCMTL*. We consider both the interval-based and point-based semantics of this logic. The verification problem that we consider is to determine if a given HCMTL* formula ℑ is true in a system represented by a timed automaton. We show that this problem is undecidable. We then show that the verification problem is decidable if we consider executions upto a fixed time horizon T. Our decidability result relies on reducing the verification problem to the truth of an MSO formula over reals with a bounded time interval. 

We consider the problem of checking the differential privacy of online randomized algorithms that process a stream of inputs and produce outputs corresponding to each input. This paper generalizes an automaton model called DiP automata [10] to describe such algorithms by allowing multiple real-valued storage variables. A DiP automaton is a parametric automaton whose behavior depends on the privacy budget ∈. An automaton A will be said to be differentially private if, for some D, the automaton is D∈-differentially private for all values of ∈ > 0. We identify a precise characterization of the class of all differentially private DiP automata. We show that the problem of determining if a given DiP automaton belongs to this class is PSPACE-complete. Our PSPACE algorithm also computes a value for D when the given automaton is differentially private. The algorithm has been implemented, and experiments demonstrating its effectiveness are presented. 

Games and competitions enhance student engagement and help improve hands-on learning of computing concepts. Focusing on targeted goals, competitions provide a sense of community and accomplishment among students, fostering peer-learning opportunities. Despite these benefits of motivating and enhancing student learning, the impact of competitions on curricular learning outcomes has not been sufficiently studied. For institutional or program accreditation, understanding the extent to which students achieve course or program learning outcomes is essential, and helps in establishing continuous improvement processes for the program curriculum. Utilizing the Collegiate Cyber Defense Competition (CCDC), a curricular assessment was conducted for an undergraduate cybersecurity program at a US institution. This archetypal competition was selected as it provides an effective platform for broader program learning outcomes, as students need to: (1) function in a team and communicate effectively (teamwork and communication skills); (2) articulate technical information to non-technical audiences (communication skills); (3) apply excellent technical and non-technical knowledge (design and analysis skills applied to problem-solving); and (4) function well under adversity (real-world problem-solving skills). Using data for both students who competed and who did not, student progress was tracked over five years. Preliminary analysis showed that these competitions made marginally-interested students become deeply engaged with the curriculum; broadened participation among women who became vital to team success by showcasing their technical and management skills; and pushed students to become self-driven, improving their academic performance and career placements. This experience report also reflects on what was learned and outlines the next steps for this work. 

Automated reasoning tools for security protocols model protocols as non-deterministic processes that communicate through a Dolev-Yao attacker. There are, however, a large class of protocols whose correctness relies on an explicit ability to model and reason about randomness. Although such protocols lie at the heart of many widely adopted systems for anonymous communication, they have so-far eluded automated verification techniques. We propose an algorithm for reasoning about safety properties for randomized protocols. The algorithm is implemented as an extension of Stochastic Protocol ANalyzer (Span), the mechanized tool that reasons about the indistinguishability properties of randomized protocols. Using Span, we conduct the first automated verification on several randomized security protocols and uncover previously unknown design weaknesses in several of the protocols we analyzed. 

Termination checking is a classic static analysis, and, within this focus, there are type-based approaches that formalize termination analysis as type systems (i.e., so that all well-typed programs terminate). But there are situations where a stronger termination property (which we call strongly-bounded termination) must be determined and, accordingly, we explore this property via a variant of the simply-typed λ-calculus called the bounded-time λ-calculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating strongly-bounded termination and BTC are described as well.